es:ES, A, V:Type, i:Id, knd:Knd, ds:x:Id fp Type, f:(State(ds)V(A + Top)).
(e:E. (loc(e) = i)  (kind(e) = knd)  ((valtype(e) r V) & (state@loc(e) r State(ds))))
 (e:E.
 ((e  es-trigger(es;i;knd;ds;f)))
  (es-trigger(es;i;knd;ds;f)(e) = outl(f((state when e),val(e)))  A)) 

latex

Definitions

False, P  Q, x:A. B(x), P  Q, b, ff, x:AB(x), P  Q, x:A  B(x), Id, s = t, A, P & Q, P  Q, Knd, t  T, val(e), ES, Type, Atom$n, left + right, a:A fp B(a), t.1, E, A c B, (state when e), if b then t else f fi , valtype(e), state@i, State(ds), f(a), Top, isl(x), outl(x), , <a, b>, , True, T, Unit, do-apply(f;x), can-apply(f;x), X(e), es-trigger(es;i;knd;ds;f), e  X, loc(e), a = b, kind(e), a = b, p  q

Lemmas

eqtt to assert, assert of band, eqff to assert, bnot thru band, assert of bor, iff transitivity, assert of bnot, assert-eq-id, and functionality wrt iff, outl wf, assert wf, isl wf, es-state-when wf, es-val wf, or functionality wrt iff, not functionality wrt iff, assert-eq-knd